\begin{tabbing}
$M_{1}$ $\oplus$ $M_{2}$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$ma\{\=fpf{-}join(IdDeq;$M_{1}$.1;$M_{2}$.1);\+
\\[0ex]fpf{-}join(KindDeq;($M_{1}$.2).1;($M_{2}$.2).1);
\\[0ex]fpf{-}join(IdDeq;($M_{1}$.2.2).1;($M_{2}$.2.2).1);
\\[0ex]fpf{-}join(IdDeq;($M_{1}$.2.2.2).1;($M_{2}$.2.2.2).1);
\\[0ex]fpf{-}join(product{-}deq(Knd;Id;KindDeq;IdDeq);($M_{1}$.2.2.2.2).1;($M_{2}$.2.2.2.2).1);
\\[0ex]fpf{-}join(product{-}deq(Knd;IdLnk;KindDeq;IdLnkDeq);($M_{1}$.2.2.2.2.2).1;($M_{2}$.2.2.2.2.2).1);
\\[0ex]fpf{-}join(IdDeq;($M_{1}$.2.2.2.2.2.2).1;($M_{2}$.2.2.2.2.2.2).1);
\\[0ex]fpf{-}join(product{-}deq(IdLnk;Id;IdLnkDeq;IdDeq);($M_{1}$.2.2.2.2.2.2.2).1;($M_{2}$.2.2.2.2.2.2.2).1);
\\[0ex]fpf{-}join(KindDeq;($M_{1}$.2.2.2.2.2.2.2.2).1;($M_{2}$.2.2.2.2.2.2.2.2).1);
\\[0ex]fpf{-}join(KindDeq;($M_{1}$.2.2.2.2.2.2.2.2.2).1;($M_{2}$.2.2.2.2.2.2.2.2.2).1);
\\[0ex]fpf{-}join(IdDeq;($M_{1}$.2.2.2.2.2.2.2.2.2.2).1;($M_{2}$.2.2.2.2.2.2.2.2.2.2).1);
\\[0ex]fpf{-}join(IdDeq;($M_{1}$.2.2.2.2.2.2.2.2.2.2.2).1;($M_{2}$.2.2.2.2.2.2.2.2.2.2.2).1)\}
\-
\end{tabbing}